

\aux{ciaNumbers}{as: [Atleta]}{[\ent]}{\comp{ciaNumber(a)}{a \selec as}}
\aux{competencias}{j: JJOO}{[Competencia]}{\comp{c}{d \selec [1..cantDias(j)], c \selec cronograma(j, d)}}
\aux{incluida}{$l_1$, $l_2$:[T]}{\bool}{(\forall x \selec l_1) cuenta(x, l_1) \leq cuenta(x, l_2)}
\aux{lasPasadasFinalizaron}{j: JJOO}{\bool}{(\forall d \selec [1..jornadaActual(j)))(\forall c \selec cronograma(j, d))finalizada(c)}
\aux{lasQueNoPasaronNoFinalizaron}{j: JJOO}{\bool}{\\(\forall d \selec (jornadaActual(j)..cantDias(j)]) (\forall c \selec cronograma(j, d))\neg finalizada(c)}
\aux{ordenada}{l:[T]}{\bool}{(\forall i \selec [0.. \longitud{l}-1)) l_i \leq l_{i+1}}
\aux{sinRepetidos}{l: [T]}{\bool}{(\forall i, j \selec [0.. \longitud{l}), i \neq j) l_i \neq l_j}








